[38;2;117;113;94m-- some code in Idris[0m
[38;2;249;38;114mmodule[0m[38;2;248;248;242m [0m[38;2;166;226;46mXX.X'''[0m

[38;2;249;38;114mimport[0m[38;2;248;248;242m [0m[38;2;166;226;46mData.Nat[0m

[38;2;249;38;114mdata[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mX[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mA[0m[38;2;248;248;242m [0m[38;2;249;38;114m|[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mB[0m

[38;2;249;38;114mnamespace[0m[38;2;248;248;242m [0m[38;2;166;226;46mX[0m
[38;2;248;248;242m  [0m[38;2;117;113;94m||| Documentation[0m
[38;2;248;248;242m  [0m[38;2;249;38;114mrecord[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mY[0m[38;2;248;248;242m [0m[38;2;249;38;114mwhere[0m
[38;2;248;248;242m    [0m[38;2;249;38;114m[[0m[38;2;248;248;242mnoHints[0m[38;2;249;38;114m][0m
[38;2;248;248;242m    [0m[38;2;249;38;114mconstructor[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mMkY'[0m
[38;2;248;248;242m    [0m[38;2;166;226;46mfield1[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m
[38;2;248;248;242m    [0m[38;2;248;248;242m{[0m[38;2;249;38;114mauto[0m[38;2;248;248;242m [0m[3;38;2;253;151;31mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m

[38;2;249;38;114mnamespace[0m[38;2;248;248;242m [0m[38;2;166;226;46mX'[0m[38;2;248;248;242m [0m[38;2;249;38;114m{[0m
[38;2;248;248;242m  [0m[38;2;249;38;114mparameters[0m[38;2;248;248;242m [0m[38;2;248;248;242m([0m[3;38;2;253;151;31mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mA[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mMaybe[0m[38;2;248;248;242m b[0m[38;2;249;38;114m)[0m[38;2;248;248;242m)[0m
[38;2;248;248;242m    [0m[38;2;166;226;46mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m
[38;2;249;38;114m}[0m

[38;2;166;226;46mu[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239m()[0m
[38;2;248;248;242mu [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239m()[0m

[38;2;166;226;46mk[0m[38;2;248;248;242m, [0m[38;2;166;226;46mw[0m[38;2;248;248;242m, [0m[38;2;166;226;46mu[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mChar[0m
[38;2;248;248;242mk [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\NUL[0m[38;2;190;132;255m'[0m
[38;2;248;248;242mw [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255mw[0m[38;2;190;132;255m'[0m

[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m[[0m[38;2;190;132;255m1[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m3[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;230;219;116m"[0m[38;2;230;219;116msdf[0m[38;2;248;248;242m\{[0m[38;2;248;248;242md[0m[38;2;248;248;242m}[0m[38;2;230;219;116m"[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0xFF[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0o77[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m0b10_1[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m100_100[0m[38;2;249;38;114m][0m

[38;2;166;226;46mf[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mInt[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mInt[0m
[38;2;248;248;242mf [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114mif[0m[38;2;248;248;242m x [0m[38;2;249;38;114m>[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114mthen[0m[38;2;248;248;242m x [0m[38;2;249;38;114melse[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[3;38;2;102;217;239m()[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mSS[0m[38;2;248;248;242m [0m[38;2;249;38;114m`[0m[38;2;249;38;114melem[0m[38;2;249;38;114m`[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mS[0m[38;2;248;248;242m [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[38;2;249;38;114mdo[0m
[38;2;248;248;242m  x [0m[38;2;249;38;114m<-[0m[38;2;248;248;242m a [0m[38;2;249;38;114m[[0m[38;2;190;132;255m1[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m2[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;190;132;255m3[0m[38;2;249;38;114m][0m
[38;2;248;248;242m  [0m[38;2;249;38;114mlet[0m[38;2;248;248;242m ukuk [0m[38;2;249;38;114m=[0m[38;2;248;248;242m akak[0m
[38;2;248;248;242m  [0m[38;2;249;38;114mrewrite[0m[38;2;248;248;242m [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m [0m[38;2;166;226;46mWow.[0m[3;38;2;102;217;239mWow[0m[38;2;248;248;242m b [0m[3;38;2;102;217;239mW[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mW[0m[38;2;249;38;114m)[0m
[38;2;248;248;242m  pure [0m[38;2;249;38;114m$[0m[38;2;248;248;242m f [0m[3;38;2;102;217;239mA[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mB[0m[38;2;248;248;242m c [0m[3;38;2;102;217;239mD[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mEE[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mE[0m

[38;2;166;226;46m(&&&)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m
[38;2;248;248;242mz [0m[38;2;249;38;114m&&&[0m[38;2;248;248;242m y [0m[38;2;249;38;114m=[0m[38;2;248;248;242m d [0m[38;2;249;38;114m+[0m[38;2;248;248;242m [0m[38;2;248;248;242m?foo[0m
[38;2;249;38;114m([0m[38;2;248;248;242m&&&[0m[38;2;249;38;114m)[0m[38;2;248;248;242m x y [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;248;248;242m?asfda[0m

[38;2;249;38;114mpublic[0m[38;2;248;248;242m [0m[38;2;249;38;114mexport[0m[38;2;248;248;242m [0m[38;2;249;38;114mcovering[0m
[38;2;166;226;46m(.fun)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mX[0m[38;2;248;248;242m a [0m[3;38;2;102;217;239mY[0m[38;2;248;248;242m b [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m
[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m.[0m[38;2;248;248;242mfun [0m[38;2;249;38;114m=[0m[38;2;248;248;242m haha[0m[38;2;249;38;114m.[0m[38;2;248;248;242mfun haha [0m[38;2;249;38;114m.[0m[38;2;248;248;242mN[0m
[38;2;249;38;114m([0m[38;2;249;38;114m.[0m[38;2;248;248;242mfun[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m ahah [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[38;2;249;38;114m\case[0m
[38;2;248;248;242m  x[0m[38;2;249;38;114m@[0m[38;2;249;38;114m([0m[38;2;248;248;242mx[0m[38;2;249;38;114m,[0m[38;2;248;248;242m y[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m [0m[38;2;166;226;46mPrelude.Types.[0m[38;2;248;248;242mahahah[0m

[38;2;166;226;46m(.N)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m
[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m.[0m[38;2;248;248;242mN [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m
[38;2;249;38;114m([0m[38;2;249;38;114m.[0m[38;2;248;248;242mN[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mS[0m[38;2;248;248;242m n[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[38;2;249;38;114m.[0m[38;2;248;248;242mN[0m[38;2;249;38;114m)[0m[38;2;248;248;242m n[0m

[38;2;166;226;46mxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mName[0m
[38;2;248;248;242mxx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m`{[0m[38;2;166;226;46mFull.[0m[3;38;2;102;217;239mName[0m[38;2;249;38;114m}[0m

[38;2;249;38;114minfixr[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114m^^^[0m[38;2;249;38;114m,[0m[38;2;248;248;242m [0m[38;2;249;38;114m&&&[0m

[38;2;166;226;46mxxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[38;2;248;248;242m?[0m
[38;2;248;248;242mxxx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114mcase[0m[38;2;248;248;242m x [0m[38;2;249;38;114mof[0m
[38;2;248;248;242m  [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m lalalaCamelCase[0m
[38;2;248;248;242m  z [0m[38;2;249;38;114m=>[0m[38;2;248;248;242m alalalCamelCase[0m

[38;2;166;226;46mff[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mTTImp[0m
[38;2;248;248;242mff [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m val[0m
[38;2;248;248;242mff [0m[38;2;190;132;255m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m`([0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;248;248;242mval [0m[38;2;249;38;114m^~^[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;249;38;114m([0m[38;2;248;248;242mabc[0m[38;2;249;38;114m)[0m[38;2;249;38;114m)[0m
[38;2;248;248;242mff [0m[38;2;190;132;255m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m f [0m[38;2;249;38;114m`([0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;248;248;242mval [0m[38;2;249;38;114m^~^[0m[38;2;248;248;242m [0m[38;2;249;38;114m~[0m[38;2;249;38;114m([0m[38;2;248;248;242mabc[0m[38;2;249;38;114m)[0m[38;2;249;38;114m)[0m[38;2;248;248;242m x[0m

[38;2;249;38;114m%language[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mElabReflection[0m
[38;2;249;38;114m%runElab[0m[38;2;248;248;242m [0m[38;2;166;226;46mX.[0m[38;2;248;248;242msf ads[0m

[38;2;249;38;114m%macro[0m[38;2;248;248;242m [0m[38;2;249;38;114m%inline[0m
[38;2;166;226;46mfff[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mList[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mDecl[0m
[38;2;248;248;242mfff [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;249;38;114m`[[0m
[38;2;248;248;242m  [0m[38;2;166;226;46mf[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m

[38;2;248;248;242m  f [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m haha [0m[38;2;249;38;114m%runElab[0m[38;2;248;248;242m [0m[38;2;249;38;114m%search[0m[38;2;248;248;242m [0m[38;2;249;38;114m@[0m[38;2;249;38;114m{[0m[38;2;249;38;114m%World[0m[38;2;249;38;114m}[0m
[38;2;249;38;114m][0m

[38;2;249;38;114mprivate[0m[38;2;248;248;242m [0m[38;2;249;38;114minfixr[0m[38;2;248;248;242m [0m[38;2;190;132;255m4[0m[38;2;248;248;242m [0m[38;2;249;38;114m^--^[0m

[38;2;249;38;114m([0m[38;2;249;38;114m^--^[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m
[38;2;249;38;114m([0m[38;2;249;38;114m^--^[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mZ[0m
[38;2;248;248;242mx [0m[38;2;249;38;114m^--^[0m[38;2;248;248;242m y [0m[38;2;249;38;114m=[0m[38;2;248;248;242m x [0m[38;2;249;38;114m+[0m[38;2;248;248;242m y[0m

[38;2;166;226;46mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[38;2;248;248;242m([0m[3;38;2;253;151;31my[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mVect[0m[38;2;248;248;242m n [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mMaybe[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[3;38;2;102;217;239mMaybe[0m[38;2;248;248;242m [0m[38;2;249;38;114m([0m[38;2;248;248;242m&&&[0m[38;2;249;38;114m)[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;249;38;114m)[0m[38;2;249;38;114m)[0m[38;2;248;248;242m)[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m
[38;2;248;248;242m    [0m[38;2;248;248;242m{[0m[3;38;2;253;151;31mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[38;2;248;248;242m{[0m[38;2;249;38;114mauto[0m[38;2;248;248;242m [0m[3;38;2;253;151;31m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mMonoid[0m[38;2;248;248;242m a[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m
[38;2;248;248;242m    [0m[38;2;248;248;242m{[0m[38;2;249;38;114mdefault [0m[38;2;249;38;114m4[0m[38;2;248;248;242m [0m[3;38;2;253;151;31mxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m
[38;2;248;248;242m    [0m[38;2;248;248;242m{[0m[38;2;249;38;114mdefault [0m[38;2;249;38;114m(f x Y)[0m[38;2;248;248;242m [0m[3;38;2;253;151;31mxx'[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m}[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m
[38;2;248;248;242m    [0m[3;38;2;102;217;239mString[0m
[38;2;248;248;242mx [0m[3;38;2;102;217;239mZ[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mS[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;248;248;242m?foo[0m
[38;2;248;248;242mx y [0m[38;2;190;132;255m_[0m[38;2;248;248;242m [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;230;219;116m"[0m[38;2;230;219;116ma b [0m[38;2;248;248;242m\{[0m[38;2;248;248;242mshow [0m[38;2;249;38;114m$[0m[38;2;248;248;242m [0m[38;2;249;38;114mlet[0m[38;2;248;248;242m x [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0[0m[38;2;248;248;242m [0m[38;2;249;38;114min[0m[38;2;248;248;242m y[0m[38;2;248;248;242m}[0m[38;2;230;219;116m y >>= z[0m[38;2;230;219;116m"[0m

[38;2;166;226;46mmultiline[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mString[0m
[38;2;248;248;242mmultiline [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m
[38;2;230;219;116m  A multiline string[0m[38;2;190;132;255m\NUL[0m
[38;2;230;219;116m  [0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m[38;2;230;219;116m"[0m

[38;2;166;226;46mf'[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m[38;2;248;248;242m [0m[38;2;249;38;114m->[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mNat[0m
[38;2;248;248;242mf' [0m[38;2;249;38;114m=[0m[38;2;248;248;242m x' [0m[38;2;190;132;255m4[0m

[38;2;166;226;46mx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mChar[0m
[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\BEL[0m[38;2;190;132;255m'[0m
[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\\[0m[38;2;190;132;255m'[0m
[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\'[0m[38;2;190;132;255m'[0m
[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255m\o755[0m[38;2;190;132;255m'[0m
[38;2;248;248;242mx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m'[0m[38;2;190;132;255ma[0m[38;2;190;132;255m'[0m

[38;2;166;226;46mxx[0m[38;2;248;248;242m [0m[38;2;249;38;114m:[0m[38;2;248;248;242m [0m[3;38;2;102;217;239mInt[0m
[38;2;248;248;242mxx [0m[38;2;249;38;114m=[0m[38;2;248;248;242m [0m[38;2;190;132;255m0o7_5_5[0m
